Nuprl Lemma : normalize-constraint_wf
11,40
postcript
pdf
k
:
,
A
:(
:(
)
). normalize-constraint(
k
;
A
)
(
:(
)
)
latex
Definitions
,
Y
,
map(
f
;
as
)
,
map-eval(
x
.
f
(
x
);
L
)
,
P
Q
,
has-value(
a
)
,
normalize-constraint(
k
;
p
)
,
t
T
,
x
:
A
.
B
(
x
)
,
,
P
&
Q
,
i
j
<
k
,
{
i
..
j
}
Lemmas
select?
wf
,
map
wf
,
le
wf
,
rational-has-value
,
int
seg
wf
,
upto
wf
,
rationals
wf
,
nat
wf
origin
k:
, A:(:(
) 
). normalize-constraint(k;A) 
(:() ) k:, A:(:() ). normalize-constraint(k;A) (:() ) 
Q Tx:A. B(x)
j < k
}